FDL - Nuprl Lemma : div_rec_case

Nuprl Lemma : div_rec_case

a:

, n:

. (a

n )

((a

n) = ((a - n)

n)+1)

Up int 2, int 2

Definitions t T, P Q, x:A. B(x), , False, A, P Q, P Q, A B, P & Q, i j , , Div(a;n;q), i j < k, , {T}, x:A. B(x)

Lemmas nat wf, nat plus wf, ge wf, le wf, div elim, add mono wrt le rw, div unique, add cancel in le, add cancel in lt